r, s:. CoPrime(r,s)  (a, b:. x:. (x = a mod r) & (x = b mod s)) 

latex

Definitions	P  Q, CoPrime(a,b), x:A. B(x), t  T, , x:A. B(x), P & Q, Prop, a = b mod m, P  Q, P  Q, T, True
Lemmas	true wf, squash wf, eqmod weakening, multiply functionality wrt eqmod, add functionality wrt eqmod, eqmod functionality wrt eqmod, eqmod wf, gcd p sym, chrem exists aux, nat plus wf, coprime wf